1. Field of the Invention
The present invention relates to an apparatus and method for verifying a logical device for use in verifying all units which can be modelled as a finite state machine, for example, a sequential circuit and a protocol.
2. Description of the Related Art
A model check is well known as a method for verifying whether or not the design of a sequential circuit and a protocol satisfies the properties required for them. This method mathematically proves that a finite state machine satisfies or does not satisfy the property represented by a temporal logic.
A general form of a finite state machine can be represented by M=(Q, xcexa3, "PHgr", xcex4, xcex, I).
Each of the symbols has the following meaning.
Q: set of states (finite)
xcexa3: input alphabet (finite)
"PHgr": output alphabet (finite)
xcex4: transition relation function
xcex: output relation function
I: initial set of states
The transition relation function is a function set to 1 if the current state can be transient to the next state when the current state, the next state, and an input are entered, and otherwise set to 0. Although the transition relation function is a function for determining the next state, it is also able to represent a nondeterministic transition in which the next state cannot be uniquely determined by a current state and an input. When the transition is deterministic, the state transition can be represented as a function for obtaining the next state by the current state and an input. The above described output relation function similarly corresponds to the case where an output is nondeterministic.
Basically, all sequential circuits can be modelled as finite state machines. Therefore, when a logical device is designed, the finite state machine is popularly used as specification. For example, in synthesizing a logic, specification of a device is described by design description language. The description is converted by a synthesizing system to a finite state machine. Then, a state is realized by a flip-flop circuit or a register, and a transition relation function 6 and an output relation function xcex are realized by a combinational circuit.
The basic theory of the above described finite state machine is described in detail in chapter 2 of the reference document 1. In verifying a logical device, it is checked whether the operation of the logical device in the time sequence satisfies a required property. An applicable technology to attain the verification can be logical simulation and a model check.
The above described logical simulation is a process of simulating an operation by applying an appropriate input to a model of a device (description in design description language, gate level circuit chart, etc.). It is confirmed that an obtained operation satisfies the property.
A model check refers to an approach in which a logical device is modelled as a finite state machine or a network of a plurality of finite state machines, and it is mathematically determined whether or not the model satisfies the property. The model check is described in detail in the special articles (reference documents 2, 3, 4, 5, and 6 described later) in the Information Processing in September in 1994.
At present, the most practical model checking method is a symbol model checking method (refer to the reference documents 7 and 8 described later). In the symbol model checking method, the operation of the finite state machine is represented by a logical expression, and the verification procedure is realized by a logical function process. At this time, a logical function is represented by a binary decision diagram (BDD) (refer to the reference documents 9, 10, 11, 12, and 13 described later). To operate a finite state machine having an enormous number of states, an implicit expressing method using a logical function and an efficient logical function process using BDD are indispensable.
FIG. 1 shows the conventional technology, that is, an example of the finite state machine. In the above described model checking method, the symbol model checking method represents a logical device model of the Kripke structure using a logical function, checks whether or not a non-empty set of states which satisfies the specification represented by a computation tree logic exists.
The Kripke structure is a kind of nondeterministic finite automaton represented by the following equation using the finite set S of states, the transition relation R of states, the set Si of an initial state point, and the set L of a source proposition which is true in each state.
K=(S, R, Si, L)
The computation tree logic is a kind of a temporal logic, and is represented by an operator A indicating xe2x80x98universalxe2x80x99, an operator E indicating xe2x80x98existentialxe2x80x99, a temporal operator F indicating xe2x80x98futurexe2x80x99, a temporal operator G indicating xe2x80x98globalxe2x80x99, a temporal operator X indicating xe2x80x98nextxe2x80x99, and a temporal operator U indicating xe2x80x98untilxe2x80x99in addition to a common logic operator.
For example, the temporal operator AGa indicates that the logical expression a exists in the set of states reachable from the initial state. In this case, in a model of a logical device, all paths reachable from the initial state are traced, and it is checked whether or not all the paths can reach the state in which the logical expression a exists.
That is, the verifying operation in the symbol model checking method is an operation of tracing the state transition of the Kripke structure and confirming whether or not the computation tree logic indicating the specification exists in each state. This operation performs a set reduction operation for obtaining the smallest fixed point or the largest fixed point in a model according to a computation tree logic expression.
The above described set operation can be realized by combining an image computation Image ({q}) for obtaining a set of states reachable from a state set {q} in one state transition process with an inverse image computation Imagerev ({q}) for obtaining a set states reachable to a state set {q} in one state transition process.
For example, in the example of the finite state machine represented by a state transition between nine states q0 through q8 as shown in FIG. 1, examples of results of the image computation and the inverse image computation are represented by the following equations.
Image ({q0})={q0, q1, q2, q3 }
Image ({q0, q2})={q0, q1, q2, q3, q5}
Imagerev ({q0})={q0, q1}
Imagerev ({q5})={q1, q2, q3, q4}
In the finite state machine shown in FIG. 1, when the temporal logic AFp using the logical expression p indicating the state q8 is verified, the image computation is sequentially repeated from the initial state q0, and it is checked whether or not all paths transient from the initial state can actually reach the state q8. When the temporal logic EFp is verified, the inverse image computation is repeated from the state q8, and it is checked whether or not there is a path reaching the initial state q8.
In a common actual symbol model checking method, a set operation is replaced with a logical function process, and the logical function process becomes more efficient by representing the logical function by a binary decision diagram (BDD).
1. J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley Publishing Company, 1979.
2. Hiromi Hiraishi and Seiji Hamaguchi, xe2x80x98Formal Verifying Method based on Logical Function Processxe2x80x99, Information Process, vol. 35, No. 8, pp. 710-718, 1994.
3. Masahiro Fujita, Masami Yamazaki et al., xe2x80x98Application of Practical Design in Formal Verifying Methodxe2x80x99, Information Process, vol. 35, No. 8, pp. 719-725, 1994.
4. Shinji Kimura, xe2x80x98Formal Timing Verificationxe2x80x99, Information Process, vol. 35. No. 8, pp. 726-735, 1994.
5. Atsushi Takahara, xe2x80x98Formal Verification using Process Algebraxe2x80x99, Information Process, vol. 35, No. 8, pp. 736-741, 1994.
6. Ken""ichi Taniguchi and Atsushi Kitamichi, xe2x80x98Specification Description, Design, and Verification in Algebraic Methodxe2x80x99, Information Process, vol. 35, No. 2, pp. 742-750, 1994.
7. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, xe2x80x98Symbolic Model Checking: 1020 States and Beyondxe2x80x99, Information and Computation, vol. 98, No. 2, pp. 142-170, 1992.
8. K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.
9. R. E. Bryant, xe2x80x98Graph Based Algorithm for Boolean Function Manipulationxe2x80x99, IEEE transactions on Computers, vol. C-35, No. 8, pp. 677-691, 1986.
10. Nagisa Ishiura, xe2x80x98What is BDD?xe2x80x99, Information Process, vol. 34, No. 5, pp. 585-592, 1993.
11. Shin""ichi Minato, xe2x80x98BDD Processing Technology on Computerxe2x80x99, Information Process, vol. 34, No. 5, pp. 593-599, 1993.
12. Etsuo Watabe and Yuji Kukimoto, xe2x80x98Application of BDDxe2x80x99, Information Process, vol. 34, No. 5, pp. 600-608, 1993.
13. Masahiro Fujita, Edmund M. Clarke, Application of BDD to CADxe2x80x2, Information Process, vol. 34, No. 5, 609-616, 1993.
An operation which can be confirmed in a logical simulation is only a result of a selected and specific input string. Therefore, when there are a large number of states, performing all operations requires a very long input string and a corresponding computation time. Actually, this is next to impossible.
Generally, since there are no mechanism of mathematically recording/adjusting confirmed operations in a logical simulation, it cannot be determined that all operations have been processed. As a result, there is no proving an operation which will not occur.
A model check mathematically covers the operations of a finite state machine. However, if there are a large number of states and a finite state machine has to correspond to complicated state transition, the operations of the finite state machine actually cannot be confirmed due to the increase in the memory requirements of the computer or the time required for computation. This appears as the problem of the scale of the BDD representing transition relation and generatd during the logical function process. The scale of a BDD can be measured by the number of nodes of the BDD. In the worst case, the scale is expanded in exponential order with respect to variables.
The Applicant of the present invention previously filed Tokuganhei 9-45114 or Tokuganhei 10-1364 with the problem of the scale of the BDD solved by dividing a set of states during the verification procedure. However, the previous inventions are intended for the verification system for a specific type of property, and is not fully applicable to practical problems.
The present invention aims at providing a method and apparatus for effectively verifying a logical device such as a sequential circuit, having a large number of states by modeling the logical device using a finite state machine, etc., while appropriately adjusting the memory capacity and computation time.
The method of verifying the logical device according to the present invention includes the steps of (a) converting a set of transition sequences of finite or infinite length representing the target property of the finite state machine which is a model of a logical device to be verified into a directed graph labelled by a transition relation function, and storing the configuration information about the directed graph in the first memory; (b) storing in the second memory a set of states belonging to each node of the directed graph; (c) reading from the second memory the set of states belonging to each node on the starting side of the directed graph, referring to the configuration information of the directed graph stored in the first memory, selecting branches to be processed in a mapping operation and then performing the mapping operation corresponding to the branches Lon the set of the read states; (d) adding the mapping operation result to the set of states belonging to each node on the ending side of the branches, and storing the results in the second memory; (e) repeating the processes above in steps (c) and (d), and verifying whether or not the logical device to be verified satisfies the target property by determining whether or not the set of transition sequences indicated by the directed graph actually has elements based on the set of states stored in the second memory.
The apparatus for verifying the logical device according to the present invention includes a first storage unit for converting a set of transition sequences of finite or infinite length representing the target property of the finite state machine which is a model of a logical device to be verified into a directed graph labelled by a transition relation function, and storing the configuration information about the directed graph in the first memory; a second storage unit for storing a set of states belonging to each node, corresponding to each node of the directed graph; a mapping operation unit for reading from the second storage unit the set of states belonging to each node on the starting side of the directed graph, referring to the configuration information of the directed graph stored in the first storage unit, selecting branches to be processed in a mapping operation and then performing the mapping operation corresponding to the branches on the set of the read states; adding the mapping operation result to the set of states belonging to each node on the ending side of the branches; and storing the results in the second memory; and determination unit for instructing the mapping operation unit to repeat the processes above, and verifying whether or not the logical device to be verified satisfies the target property by determining whether or not the set of transition sequences indicated by the directed graph actually has elements, based on the set of states stored in the second storage unit.
According to the present invention, when a mapping operation is performed on a branch, a set of states at a node on the starting side of the branch can be arbitrarily selected. The mapping operation can be flexibly performed. For example, it can be performed only on one state, a subset, etc. Therefore, the process can be performed while the memory capacity and the computation time are appropriately adjusted. In addition, since the mapping operation is performed for each directed graph, the process can terminate when a target transition sequence is detected even if the mapping operation has not been completed on all branches, thereby saving the applicable memory capacity of the logical device and the computation time. As a result, a logical device which has a large number of states and cannot be conventionally verified can be successfully verified.